r:. (|r| * |r|) = (r * r)   

latex

Definitions	T, P & Q, P  Q, P  Q, True, ff, tt, P  Q, if b then t else f fi , , t  T, |r|, x:A. B(x), Unit, , S  T,
Lemmas	qinv inv q, true wf, squash wf, qmul over minus qrng, int inc rationals, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, assert wf, qmul wf, bool wf, qpositive wf, rationals wf